L:Knd List, l:IdLnk, tg:Id.
@source(l): only L sends on (l with tg) realizes es. only events in L send on l with tg 

latex

Definitions

t  T, x:A. B(x), ES(the_w), (Msg on l), type List, nil, x:AB(x), P & Q, A & B, {T}, P  Q, sender(e), A/x,y. B(x;y), 1of(t), E, b, sends(l,tg,e), s = t, Prop, Type, x:AB(x), False, A, Void, x:A. B(x), Top, S  T, null(as), left+right, , P  Q, P  Q, IdLnk, Atom$n, Id, Dsys, D1  D2, World, FairFifo, PossibleWorld(D;w), rcv(l,tg), kind(e), Knd, (x  l), @i: only L sends on (l with tg), D realizes es. P(es), only events in L send on l with tg, source(l), Msg, val(e), tag(e), lnk(e), msg(l;t;v), sends(l;e), {x:A| B(x) }, Msg(M), mtag(m), a = b, x.A(x), <a,b>, SQType(T), s ~ t, lnk(k), , #$n, ||as||, AB, , l[i], a<b, ij, {i..j}, i  j < k, True, T, x:A. B(x), index(e), tag(k), haslink(l;m), car.cdr, outl(x), 2of(t), mtag(m)

Lemmas

l member wf, cons one one, nat wf, member wf, tagof wf, assert-eq-id, le wf, non neg length, int seg wf, es-index wf, length wf1, select wf, Knd sq, IdLnk sq, es-lnk wf, member filter, eq id wf, es-mtag wf, es-sends wf, es-Msg wf, l member subtype, es-axioms, Id wf, IdLnk wf, sframe-rule, dsys wf, d-sub wf, d-single-sframe wf, lsrc wf, world wf, fair-fifo wf, possible-world wf, Knd wf, es-kind wf, rcv wf, es-E wf, not functionality wrt iff, assert of null, assert wf, null wf3, top wf, es-tg-sends wf, es-sender wf, es-kind-rcv, es-Msgl wf, w-es wf